(Completion Options): Add an index for "ignored file names".

diff --git a/man/mini.texi b/man/mini.texi
index 7611c7c32ea1cf400a2d345091e48a1c66cfea08..6e15d1fc6743ffa965c0cc4d2498bb6e8c09defb 100644 (file)
--- a/man/mini.texi
+++ b/man/mini.texi
@@ -360,6 +360,7 @@ the list of completions is long, you can scroll it with @kbd{C-M-v}
 @subsection Completion Options
 
 @vindex completion-ignored-extensions
+@cindex ignored file names, in completion
   When completion is done on file names, certain file names are usually
 ignored.  The variable @code{completion-ignored-extensions} contains a
 list of strings; a file whose name ends in any of those strings is